$\vdash$  $\forall$$A$:Type, $L$:($A$ List), $n$:$\mathbb{N}$. ($n$ $\leq$ $\parallel$$L$$\parallel$) $\Rightarrow$ (lastn($n$;$L$) $\in$ ($A$ List))